/*
	アドレス帳にアドレスを削除する操作を登録する
*/

module tour/addressBook3

// 名前
sig Name {}

// アドレス
sig Addr {}

// アドレス帳
sig Book { 
	addr: Name -> lone Addr
}

// 表示
pred show (b:Book) {
	// アドレス帳に1つ以上のアドレスが存在できることを確認。
	#b.addr > 1
	
	// 1つの名称に紐づくアドレスが指定した数存在できるか確認。
	// some n: Name | #n.(b.addr) < 1

	// アドレス帳のアドレスと紐づく名称が複数あるパターンを確認。
	#Name.(b.addr) > 1
}
//run show for 3 but 1 Book

// アドレス帳にアドレスを追加する操作
pred add (b, b': Book, n: Name, a: Addr) {
	b'.addr = b.addr + n -> a
}
//run add for 3 but 2 Book

// 削除する述語
pred del (b, b': Book, n: Name) {
	b'.addr = b.addr - n -> Addr
}

// 参照する関数
fun lookup(b: Book, n: Name) : set Addr {
	n.(b.addr)
}

// 追加処理を表示する
pred showAdd (b, b': Book, n: Name, a: Addr) {
	add [b, b', n, a]

	// 追加後のアドレス１つに対応する名称が複数存在するパターンがあるか確認
	#Name.(b'.addr) > 1
}
run showAdd for 3 but 2 Book

// 削除処理は追加操作のアンドゥであることを確認。
assert delUndoAdd {
	all b, b', b'': Book, n: Name, a: Addr |
		no n.(b.addr) and add[b, b', n, a] and del[b', b'', n] implies b.addr = b''.addr
}

// 追加を繰り返しても変化がない
assert addIdempotent { 
	all b, b', b'': Book, n: Name, a:Addr |
		add[b, b', n, a] and add[b', b'', n, a] implies b'.addr = b''.addr
}

// 追加をした場合に追加した名称以外のアドレスには影響ないことを確認する
assert addLocal {
	all b,b': Book, n,n': Name, a: Addr |
		add[b, b', n, a] and n != n' implies lookup[b, n'] = lookup[b', n']
}

check addIdempotent for 10 but 3 Book
check delUndoAdd for 10 but 3 Book
check addLocal for 10 but 3 Book
